Definitions | t T,  x. t(x), x:A. B(x), Void, x.A(x), f(x)?z, x:A B(x), #$n, a<b, False, P  Q, A, A B, , {x:A| B(x) }, , Atom, x:A B(x), Id, IdLnk, left+right, type List, x dom(f). v=f(x)  P(x;v), f(a), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdDeq, IdLnkDeq, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), EqDecider(T), M.dout(l,tg), da(M), MsgA, AtomFree(d), rcv(l,tg), KindDeq, Type, Knd, a:A fp B(a), AtomFree(T;x) |